Inference at * 1 
Iof proof for Lemma eq atom eq false elim sqequal:



1. x : Atom
2. y : Atom
  (x =a y ~ ff)  ((x = y)) 

latex

 by D 0 

latex

 1: 

 1: 3. x =a y ~ ff
 1:   (x = y)
 2: .....wf..... NILNIL

 2:   (x =a y ~ ff)  Type
 .

Definitions	P  Q, t  T
Lemmas	not wf